A revised attempt at ax-mulf comment wording #5032
Conversation
The ax-mulf comment is confusing. Its text "is not a bona fide axiom for complex numbers" makes it sound like this statement can't be an axiom or that Metamath can't handle such axioms, which is obviously untrue. Also, the cited paper doesn't justify this axiom. This commit attempts to clarify the comment for ax-mulf in the hopes of making it clearer. Signed-off-by: David A. Wheeler <[email protected]>
This is in response to discussion on github and includes: - focus on the consequences of using it or not, with less language about which we prefer (because there doesn't seem to be a consensus about that). - compare with other operations - refer to mulcl rather than ax-mulcl directly - mention mpomulf
| $( Multiplication is an operation on the complex numbers. This is the | ||
| construction-dependent version of ~ ax-mulf and it should not be |
There was a problem hiding this comment.
should ax-mulf be mulcl here?
There was a problem hiding this comment.
No, this sentence is contrasting ax-mulf and axmulf. The following sentence is about axmulf (or ax-mulf) versus mulcl
There was a problem hiding this comment.
I don't really understand how one theorem is the construction-dependent version of the other when they're both the same - by my understanding both are construction-dependent.
There was a problem hiding this comment.
The "construction-dependent" wording is not new and is used throughout this section (see for example https://us.metamath.org/mpeuni/ax1cn.html ).
We could consider that phrasing in another issue or pull request; I'm not sure I have an immediate thought about alternate wordings for this $j restatement situation.
There was a problem hiding this comment.
Ah I see, I mixed up the notion of the result of axmulf/ax-mulf as a property depending on the certain definition of multiplication, vs whether axmulf/ax-mulf is proven from, i.e. dependent on, the construction of complex numbers or stated as an axiom.
The wording makes sense now
6 participants
I have read over #4796 and attempted to incorporate the suggestions made on that issue (although the more I looked at it, the more it seemed like a slightly bigger rewording seemed to be called for).
Glad to discuss specific points but I guess for now I'll just refer to the discussion there and the commit message I have added in this pull request. I have kept @david-a-wheeler 's changes and mine in separate commits in case that makes it easier to review.